Nuprl Lemma : eq_id_self
0,22
postcript
pdf
a
:Id.
a
=
a
~ true
latex
Definitions
t
T
,
IdDeq
,
Id
,
x
:
A
.
B
(
x
)
,
a
=
b
,
true
Lemmas
bool
sq
,
eqof
eq
btrue
,
Id
wf
,
id-deq
wf
origin
a:Id. a = a ~ true
a:Id. a = a ~ true 
Tx:A. B(x)